g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
f(s(x), y) → f(half(s(x)), double(y))
f(s(0), y) → y
id(x) → f(x, s(0))
↳ QTRS
↳ DependencyPairsProof
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
f(s(x), y) → f(half(s(x)), double(y))
f(s(0), y) → y
id(x) → f(x, s(0))
HALF(x) → G(h, x)
F(s(x), y) → HALF(s(x))
ID(x) → F(x, s(0))
DOUBLE(x) → G(d, x)
F(s(x), y) → DOUBLE(y)
F(s(x), y) → F(half(s(x)), double(y))
G(h, s(s(x))) → G(h, x)
G(d, s(x)) → G(d, x)
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
f(s(x), y) → f(half(s(x)), double(y))
f(s(0), y) → y
id(x) → f(x, s(0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
HALF(x) → G(h, x)
F(s(x), y) → HALF(s(x))
ID(x) → F(x, s(0))
DOUBLE(x) → G(d, x)
F(s(x), y) → DOUBLE(y)
F(s(x), y) → F(half(s(x)), double(y))
G(h, s(s(x))) → G(h, x)
G(d, s(x)) → G(d, x)
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
f(s(x), y) → f(half(s(x)), double(y))
f(s(0), y) → y
id(x) → f(x, s(0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
G(h, s(s(x))) → G(h, x)
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
f(s(x), y) → f(half(s(x)), double(y))
f(s(0), y) → y
id(x) → f(x, s(0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(h, s(s(x))) → G(h, x)
The value of delta used in the strict ordering is 3/8.
POL(s(x1)) = 1/4 + (2)x_1
POL(G(x1, x2)) = (1/2)x_2
POL(h) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
f(s(x), y) → f(half(s(x)), double(y))
f(s(0), y) → y
id(x) → f(x, s(0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
G(d, s(x)) → G(d, x)
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
f(s(x), y) → f(half(s(x)), double(y))
f(s(0), y) → y
id(x) → f(x, s(0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(d, s(x)) → G(d, x)
The value of delta used in the strict ordering is 8.
POL(d) = 0
POL(s(x1)) = 4 + (4)x_1
POL(G(x1, x2)) = (2)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
f(s(x), y) → f(half(s(x)), double(y))
f(s(0), y) → y
id(x) → f(x, s(0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
F(s(x), y) → F(half(s(x)), double(y))
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
f(s(x), y) → f(half(s(x)), double(y))
f(s(0), y) → y
id(x) → f(x, s(0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(s(x), y) → F(half(s(x)), double(y))
The value of delta used in the strict ordering is 1/2.
POL(half(x1)) = (1/2)x_1
POL(g(x1, x2)) = (1/2)x_2
POL(s(x1)) = 1/4 + x_1
POL(d) = 0
POL(h) = 0
POL(F(x1, x2)) = (4)x_1
POL(double(x1)) = 0
POL(0) = 0
g(x, 0) → 0
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
half(x) → g(h, x)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
f(s(x), y) → f(half(s(x)), double(y))
f(s(0), y) → y
id(x) → f(x, s(0))